Termination proof of /tmp/tmpNZWfmg/ExSec4_2_DLMMU04

Termination of the following Term Rewriting System could be disproven:

Generalized rewrite system (where rules with free variables on rhs are allowed):
The TRS R consists of the following rules:

splitAt(s(N), cons(X)) → u(splitAt(N, XS))
u(pair(YS, ZS)) → pair(cons(X), ZS)
tail(cons(N)) → XS
natsFrom(N) → cons(N)
fst(pair(XS, YS)) → XS
snd(pair(XS, YS)) → YS
splitAt(0, XS) → pair(nil, XS)
head(cons(N)) → N
sel(N, XS) → head(afterNth(N, XS))
take(N, XS) → fst(splitAt(N, XS))
afterNth(N, XS) → snd(splitAt(N, XS))

↳ GTRS

  ↳ CritRuleProof

Generalized rewrite system (where rules with free variables on rhs are allowed):
The TRS R consists of the following rules:

splitAt(s(N), cons(X)) → u(splitAt(N, XS))
u(pair(YS, ZS)) → pair(cons(X), ZS)
tail(cons(N)) → XS
natsFrom(N) → cons(N)
fst(pair(XS, YS)) → XS
snd(pair(XS, YS)) → YS
splitAt(0, XS) → pair(nil, XS)
head(cons(N)) → N
sel(N, XS) → head(afterNth(N, XS))
take(N, XS) → fst(splitAt(N, XS))
afterNth(N, XS) → snd(splitAt(N, XS))

The rule splitAt(s(N), cons(X)) → u(splitAt(N, XS)) contains free variables in its right-hand side. Hence the TRS is not-terminating.